\begin{tabbing}
$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{B}$), $e$:E.
\\[0ex](($\uparrow$($e$ $\in_{b}$ es{-}local{-}le{-}pred\{i:l\}(${\it es}$;$P$))) $\Leftarrow\!\Rightarrow$ ($\exists$$a$:E. ($a$ $\leq$loc $e$  \& ($\uparrow$($P$($a$))))))
\\[0ex]\& (\=($\uparrow$($e$ $\in_{b}$ es{-}local{-}le{-}pred\{i:l\}(${\it es}$;$P$)))\+
\\[0ex]$\Rightarrow$ \=(es{-}local{-}le{-}pred\{i:l\}(${\it es}$;$P$)($e$) $\leq$loc $e$ \+
\\[0ex]\& ($\uparrow$($P$(es{-}local{-}le{-}pred\{i:l\}(${\it es}$;$P$)($e$))))
\\[0ex]\& (\=$\forall$${\it e''}$:E.\+
\\[0ex]${\it e''}$ $\leq$loc $e$  $\Rightarrow$ (es{-}local{-}le{-}pred\{i:l\}(${\it es}$;$P$)($e$) $<$loc ${\it e''}$) $\Rightarrow$ ($\neg$($\uparrow$($P$(${\it e''}$)))))))
\-\-\-
\end{tabbing}